Nuprl Lemma : es-atom_wf
11,40
postcript
pdf
es
:ES,
i
:Id,
a
:Atom1.
i
||
a
latex
Definitions
Atom$n
,
x
:
A
.
B
(
x
)
,
Id
,
ES
,
i
||
a
origin
es:ES, i:Id, a:Atom1. i || a 
es:ES, i:Id, a:Atom1. i || a x:A. B(x)